$((\mathrm{sa665}=1)\land (\mathrm{sa661}=1)\land (\mathrm{csa98}=1)\land (\mathrm{csa44}=1))\lor ((\mathrm{sa2}=1)\land (\mathrm{csa20}=1))$ $(\mathrm{csa58}=1)\lor (\mathrm{csa51}=1)\lor (\mathrm{csa90}=1)\land (\mathrm{sa459}=1)$ $(\mathrm{sa668}=1)\land (\mathrm{sa667}=1)\land (\mathrm{sa669}=1)$ $(\mathrm{sa205}=1)\lor (\mathrm{csa44}=1)\lor ((\mathrm{csa84}=1)\land (\mathrm{sa219}=1)\land (\mathrm{csa20}=1))$ $((\mathrm{csa103}=1)\land (\mathrm{csa44}=1))\lor ((\mathrm{csa20}=1)\land (\mathrm{sa219}=1))$ $(\mathrm{csa24}=1)\land (\mathrm{sa500}=1)$ $(\mathrm{sa20}=1)\lor (\mathrm{sa644}=1)\lor (\mathrm{sa18}=1)\lor ((\mathrm{sa710}=1)\land (\mathrm{sa713}=0))$ $((\mathrm{csa103}=1)\land (\mathrm{csa44}=1))\lor ((\mathrm{csa34}=1)\land (\mathrm{sa253}=1))$ $(\mathrm{sa397}=1)\land (\mathrm{sa361}=1)$ $(\mathrm{csa53}=1)\lor (\mathrm{sa692}=1)\land (\mathrm{sa652}=1)$ $\mathrm{sa494}=0$ $(\mathrm{sa700}=1)\land (\mathrm{sa695}=0)$$\mathrm{sa695}=0$ $(\mathrm{sa2}=1)\land (\mathrm{csa20}=1)$ $(\mathrm{sa24}=1)\land (\mathrm{sa13}=1)\land (\mathrm{sa19}=1)\land (\mathrm{sa255}=1)\land (\mathrm{csa34}=1)$ $\mathrm{csa20}=1$ $(\mathrm{sa24}=1)\land (\mathrm{sa13}=1)\land (\mathrm{sa19}=1)\land (\mathrm{sa255}=1)\land (\mathrm{csa34}=1)$ $(\mathrm{sa24}=1)\land (\mathrm{sa13}=1)\land (\mathrm{sa19}=1)\land (\mathrm{sa255}=1)\land (\mathrm{csa34}=1)$ $(\mathrm{csa47}=1)\lor (\mathrm{sa335}=1)\land (\mathrm{sa30}=1)\land (\mathrm{sa32}=1)$ $(\mathrm{csa84}=1)\land (\mathrm{sa219}=1)\land (\mathrm{csa20}=1)$ $(\mathrm{sa24}=1)\land (\mathrm{sa13}=1)\land (\mathrm{sa19}=1)\land (\mathrm{sa255}=1)\land (\mathrm{csa34}=1)$ $\mathrm{csa47}=1$ $((\mathrm{sa355}=1)\land (\mathrm{sa364}=1))\lor (\mathrm{sa374}=1)$ $((\mathrm{sa354}=1)\land (\mathrm{sa373}=1)\land (\mathrm{sa372}=1))\lor ((\mathrm{sa360}=1)\land (\mathrm{sa371}=1)\land (\mathrm{sa358}=1))$ $((\mathrm{sa355}=1)\land (\mathrm{sa392}=1)\land (\mathrm{csa97}=1))\lor ((\mathrm{sa379}=1)\lor (\mathrm{sa378}=1)\land (\mathrm{sa355}=1)\land (\mathrm{sa381}=1))\lor ((\mathrm{sa355}=1)\land (\mathrm{sa385}=1))$ $\mathrm{sa359}=1$ $(\mathrm{sa361}=1)\lor ((\mathrm{sa397}=1)\land (\mathrm{sa361}=1))$ $(\mathrm{sa360}=1)\lor (\mathrm{sa354}=1)\lor (\mathrm{sa364}=1)\lor (\mathrm{sa355}=1)$ $((\mathrm{sa355}=1)\land (\mathrm{sa365}=1))\lor ((\mathrm{sa364}=1)\land (\mathrm{sa367}=1))$ $(\mathrm{sa355}=1)\land (\mathrm{sa365}=1)$ $(\mathrm{sa355}=1)\land (\mathrm{sa365}=1)$ $(\mathrm{sa364}=1)\land (\mathrm{sa367}=1)$ $(\mathrm{sa355}=1)\land (\mathrm{sa364}=1)$ $(\mathrm{sa355}=1)\land (\mathrm{sa364}=1)$ $(\mathrm{sa354}=1)\land (\mathrm{sa376}=1)$ $(\mathrm{sa379}=1)\lor (\mathrm{sa378}=1)\land (\mathrm{sa355}=1)\land (\mathrm{sa381}=1)$ $(\mathrm{sa380}=1)\land (\mathrm{sa382}=1)\land (\mathrm{sa384}=1)$ $(\mathrm{sa380}=1)\land (\mathrm{sa382}=1)\land (\mathrm{sa384}=1)$ $(\mathrm{sa355}=1)\land (\mathrm{sa392}=1)\land (\mathrm{csa97}=1)$ $(\mathrm{sa391}=1)\land (\mathrm{sa395}=1)\land (\mathrm{sa393}=1)$ $(\mathrm{sa391}=1)\land (\mathrm{sa395}=1)\land (\mathrm{sa393}=1)$ $(\mathrm{sa360}=1)\lor (\mathrm{csa20}=1)\land (\mathrm{csa50}=1)$ $(\mathrm{sa460}=1)\lor (\mathrm{csa56}=1)\land (\mathrm{sa652}=1)\land (\mathrm{sa653}=0)$ $(\mathrm{sa460}=1)\lor (\mathrm{csa57}=1)\lor (\mathrm{csa52}=1)$ $\mathrm{csa34}=1$$(\mathrm{sa2}=1)\land (\mathrm{csa20}=1)$ $((\mathrm{sa463}=1)\land (\mathrm{sa461}=0))\lor ((\mathrm{sa460}=1)\lor (\mathrm{csa54}=1)\lor (\mathrm{csa52}=1)\land (\mathrm{sa653}=1))$ $(\mathrm{sa652}=1)\land (\mathrm{sa461}=1)$$\mathrm{sa498}=0$ $\mathrm{sa498}=0$ $\mathrm{sa498}=0$ $\mathrm{sa498}=0$ $\mathrm{sa499}=0$ $(\mathrm{csa92}=1)\lor (\mathrm{csa93}=1)\lor (\mathrm{csa94}=1)\lor (\mathrm{csa95}=1)\land (\mathrm{sa691}=0)$ $(\mathrm{sa354}=1)\land (\mathrm{sa376}=1)$ $(\mathrm{sa354}=1)\land (\mathrm{sa376}=1)$